T:Type, n, m:, b:T, c:({0..(n+m)}TT).
primrec(n+m;b;c) = primrec(n;primrec(m;b;c);i,t. c(i+m,t))  T 

latex

ProofTree

Definitions	False, A, A  B, i  j , P  Q, t  T, x:A. B(x), tt, (i = j), if b then t else f fi , Y, primrec(n;b;c), True, T, S  T, , {T}, SQType(T), P & Q, i  j < k, suptype(S; T), {i..j}, ff, , P  Q, Unit, ,
Lemmas	ge wf, nat properties, int seg wf, nat wf, true wf, squash wf, primrec wf, le wf, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf, eq int wf